Termination Proof Script

Consider the TRS R consisting of the rewrite rules
1:    minus(x,0)  → x
2:    minus(s(x),s(y))  → minus(x,y)
3:    le(0,y)  → true
4:    le(s(x),0)  → false
5:    le(s(x),s(y))  → le(x,y)
6:    quot(0,s(y))  → 0
7:    quot(s(x),s(y))  → s(quot(minus(s(x),s(y)),s(y)))
There are 4 dependency pairs:
8:    MINUS(s(x),s(y))  → MINUS(x,y)
9:    LE(s(x),s(y))  → LE(x,y)
10:    QUOT(s(x),s(y))  → QUOT(minus(s(x),s(y)),s(y))
11:    QUOT(s(x),s(y))  → MINUS(s(x),s(y))
The approximated dependency graph contains 3 SCCs: {9}, {8} and {10}.
Tyrolean Termination Tool  (0.01 seconds)   ---  May 4, 2006